\begin{tabbing}
$\forall$$E$,$X_{1}$,$X_{2}$:Type, ${\it info}$:($E$$\rightarrow$((:Id $\times$ $X_{1}$) + (:(:IdLnk $\times$ $E$) $\times$ $X_{2}$))), ${\it pred?}$:($E$$\rightarrow$(?$E$)).
\\[0ex]wellfounded\=\{i:l\}\+
\\[0ex]($E$; $e$,${\it e'}$.(($\neg$($\uparrow$first(${\it e'}$))) c$\wedge$ ($e$ = pred(${\it e'}$) $\in$ $E$)))
\-\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ ($\forall$$e$,${\it e'}$:$E$. (loc($e$) = loc(${\it e'}$) $\in$ Id) $\Rightarrow$ (${\it pred?}$($e$) = ${\it pred?}$(${\it e'}$)) $\Rightarrow$ ($e$ = ${\it e'}$))
\\[0ex]$\Rightarrow$ \=($\forall$$e$,${\it e'}$:$E$.\+
\\[0ex](loc($e$) = loc(${\it e'}$) $\in$ Id)
\\[0ex]$\Rightarrow$ \=(($e$ rel\_plus($E$; ($\lambda$$e$,${\it e'}$. ($\neg$($\uparrow$first(${\it e'}$))) c$\wedge$ ($e$ = pred(${\it e'}$)))) ${\it e'}$)\+
\\[0ex]$\vee$ ($e$ = ${\it e'}$)
\\[0ex]$\vee$ (${\it e'}$ rel\_plus($E$; ($\lambda$$e$,${\it e'}$. ($\neg$($\uparrow$first(${\it e'}$))) c$\wedge$ ($e$ = pred(${\it e'}$)))) $e$)))
\-\-
\end{tabbing}